The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(2^n, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(2ⁿ):
The rewrite sequence
ack(s(s(x52929_1)), s(s(s(x52701_1)))) →⁺ ack(x52929_1, plus(plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))), ack(s(x52929_1), plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,0,1,0].
The pumping substitution is [x52701_1 / s(x52701_1)].
The result substitution is [ ].

The rewrite sequence
ack(s(s(x52929_1)), s(s(s(x52701_1)))) →⁺ ack(x52929_1, plus(plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))), ack(s(x52929_1), plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,1,1,1,0].
The pumping substitution is [x52701_1 / s(x52701_1)].
The result substitution is [ ].

(2) BOUNDS(2^n, INF)